es:ES, L:(Id List).
fischer(L)
 (e:E.
 fEvent(e)
  (i:.
  (j:.
  (((rank(e) = <i, (2 * j)+1>  (:  ))
  (( ((("x" after e) = "try"  Id)  (("x" after e) = "taken"  Id)))
  (& ((rank(e) = <i, (2 * j)+2>  (:  ))
  (& ( ((("x" after e) = "contending"  Id)  (("x" after e) = "mine"  Id))))
  & ((rank(e) = <i, 0>  (:  ))  (("x" after e) = "free"  Id & (0 < i))))) 

latex

Definitions	True, T, , {T}, SQType(T), t  T, P  Q, x:A. B(x), xL. P(x), @i(x:T), P  Q, @e(xv), b, P & Q, A, (x  l), A c B, (e <loc e'), fischer(L)
Lemmas	es-locl-iff, es-loc wf, es-loc-pred, Id sq